#include <stdio.h>
#include <stdlib.h>
#include <string.h>

#include "FreeRTOS.h"
#include "task.h"

_(dynamic_owns) typedef struct tskTaskControlBlock
{
	xListItem				xGenericListItem;		/*< The list that the state list item of a task is reference from denotes the state of that task (Ready, Blocked, Suspended ). */
	xListItem				xEventListItem;		/*< Used to reference a task from an event list. */
	unsigned portBASE_TYPE	uxPriority;			/*< The priority of the task.  0 is the lowest priority. */

		_(invariant uxPriority < configMAX_PRIORITIES)
		_(invariant \mine(&xGenericListItem))
		_(invariant \mine(&xEventListItem))
} tskTCB;

PRIVILEGED_DATA tskTCB * volatile pxCurrentTCB = NULL;

PRIVILEGED_DATA static xList pxReadyTasksLists[ configMAX_PRIORITIES ];	/*< Prioritised ready tasks. */
PRIVILEGED_DATA static xList xDelayedTaskList1;							/*< Delayed tasks. */
PRIVILEGED_DATA static xList xDelayedTaskList2;							/*< Delayed tasks (two lists are used - one for delays that have overflowed the current tick count. */
PRIVILEGED_DATA static xList * volatile pxDelayedTaskList ;				/*< Points to the delayed task list currently being used. */
PRIVILEGED_DATA static xList * volatile pxOverflowDelayedTaskList;		/*< Points to the delayed task list currently being used to hold tasks that have overflowed the current tick count. */
PRIVILEGED_DATA static xList xPendingReadyList;							/*< Tasks that have been readied while the scheduler was suspended.  They will be moved to the ready queue when the scheduler is resumed. */

PRIVILEGED_DATA static xList xTasksWaitingTermination;				/*< Tasks that have been deleted - but the their memory not yet freed. */

PRIVILEGED_DATA static xList xSuspendedTaskList;

_(def \bool excList(){

    \bool tmp = (
        \forall int i1, i2; ( 0 <= i1 && i1 < i2 && i2 < configMAX_PRIORITIES )
            ==> !((&pxReadyTasksLists[i1]) == (&pxReadyTasksLists[i2]))
    ) && (
        \forall int i; ( 0 <= i && i < configMAX_PRIORITIES )
            ==> (!((&pxReadyTasksLists[i]) == &xDelayedTaskList1)
              && !((&pxReadyTasksLists[i]) == &xDelayedTaskList2)
              && !((&pxReadyTasksLists[i]) == &xSuspendedTaskList)
              && !((&pxReadyTasksLists[i]) == &xTasksWaitingTermination))
    ) && (
        &xDelayedTaskList1 != &xDelayedTaskList2
    ) && (
        &xDelayedTaskList1 != &xSuspendedTaskList
    ) && (
        &xDelayedTaskList1 != &xTasksWaitingTermination
    ) && (
        &xDelayedTaskList2 != &xSuspendedTaskList
    ) && (
        &xDelayedTaskList2 != &xTasksWaitingTermination
    ) && (
        &xSuspendedTaskList != &xTasksWaitingTermination
    );

    return tmp;
})

PRIVILEGED_DATA static xTaskHandle xIdleTaskHandle = NULL;			/*< Holds the handle of the idle task.  The idle task is created automatically when the scheduler is started. */

PRIVILEGED_DATA static volatile signed portBASE_TYPE xSchedulerRunning 			= pdFALSE;

#define prvGetTCBFromHandle( pxHandle ) ( ( ( pxHandle ) == NULL ) ? ( tskTCB * ) pxCurrentTCB : ( tskTCB * ) ( pxHandle ) )

_(ghost typedef tskTCB * TASK;)

_(ghost _(dynamic_owns) typedef struct{
	\bool tasks[TASK];
    STATE state[TASK];
    //CONTEXT phys_context;
    //CONTEXT log_context[TASK];

    \natural priority[TASK];

    //READY
    _(invariant \forall TASK t; (tasks[t] && xSchedulerRunning != pdFALSE) ==>
        ((((xList *)((tskTCB *) t)->xGenericListItem.pvContainer) == &pxReadyTasksLists[((tskTCB *) t)->uxPriority] &&
         ((tskTCB *) t) != pxCurrentTCB) <==> state[t] == ready))
    //BLOCKED
    _(invariant \forall TASK t; (tasks[t] && xSchedulerRunning != pdFALSE) ==>
        ((((xList *)((tskTCB *) t)->xGenericListItem.pvContainer) == &xDelayedTaskList1 ||
          ((xList *)((tskTCB *) t)->xGenericListItem.pvContainer) == &xDelayedTaskList2) <==> state[t] == blocked))
    //SUSPENDED
    _(invariant \forall TASK t; (tasks[t] && xSchedulerRunning != pdFALSE) ==>
        (((xList *)((tskTCB *) t)->xGenericListItem.pvContainer) == &xSuspendedTaskList <==> state[t] == suspended))
    //RUNNING
    _(invariant \forall TASK t; (tasks[t] && xSchedulerRunning != pdFALSE) ==>
        (t == (TASK) pxCurrentTCB <==> state[t] == running))
    _(invariant ((xList *) pxCurrentTCB->xGenericListItem.pvContainer) == &pxReadyTasksLists[pxCurrentTCB->uxPriority])
    //NONEXISTENT
    _(invariant \forall TASK t; (t->\closed && xSchedulerRunning != pdFALSE) ==>
        ((((xList *)((tskTCB *) t)->xGenericListItem.pvContainer) == &xTasksWaitingTermination ||
          t == NULL) <==> state[t] == nonexistent))
  
    _(invariant \forall TASK t; xSchedulerRunning != pdFALSE ==> (state[t] != nonexistent <==> tasks[t]))
    _(invariant \forall TASK t; tasks[t] ==> \mine(t))
	_(invariant \forall TASK t; tasks[t] ==> t->\closed)
    _(invariant \forall TASK t; tasks[t] ==> priority[t] == t->uxPriority)
	_(invariant \forall TASK t; tasks[t] ==> state[t] <= 4)
    _(invariant \mine(\embedding(& xIdleTaskHandle)))
    _(invariant \mine(\embedding(& pxCurrentTCB)))
	_(invariant xSchedulerRunning != pdFALSE ==> (tasks[xIdleTaskHandle] && tasks[pxCurrentTCB]))
    _(invariant xSchedulerRunning != pdFALSE && xIdleTaskHandle != NULL ==> priority[xIdleTaskHandle] == 0)
    _(invariant \forall TASK t; xSchedulerRunning != pdFALSE && state[t] == ready ==> priority[pxCurrentTCB] >= priority[t])
} * FRTOS;)

//signed portBASE_TYPE xTaskGenericCreate(unsigned portBASE_TYPE uxPriority, xTaskHandle *pxCreatedTask _(ghost FRTOS FreeRTOS) _(ghost TASK *newTask))
signed portBASE_TYPE xTaskGenericCreate( pdTASK_CODE pxTaskCode, const signed char * const pcName, unsigned short usStackDepth, void *pvParameters, unsigned portBASE_TYPE uxPriority, xTaskHandle *pxCreatedTask, portSTACK_TYPE *puxStackBuffer, const xMemoryRegion * const xRegions _(ghost FRTOS FreeRTOS) _(ghost TASK *newTask) )
	_(updates FreeRTOS)
	_(requires xSchedulerRunning == pdTRUE)
    _(requires excList())

	//_(writes newTask, pxCreatedTask, 
 //       &pxReadyTasksLists[uxPriority >= configMAX_PRIORITIES ? configMAX_PRIORITIES - ( unsigned portBASE_TYPE ) 1U : uxPriority],
 //       \embedding(&pxReadyTasksLists[uxPriority >= configMAX_PRIORITIES ? configMAX_PRIORITIES - ( unsigned portBASE_TYPE ) 1U : uxPriority]))
    _(writes newTask, pxCreatedTask)

    _(ensures \result == pdPASS ==> uxPriority > \old(pxCurrentTCB)->uxPriority ==> (FreeRTOS->state[(TASK)\old(pxCurrentTCB)]) == ready && (FreeRTOS->state[(TASK)pxCurrentTCB]) == running)
    _(ensures \result == pdPASS ==> uxPriority <= \old(pxCurrentTCB)->uxPriority ==> (FreeRTOS->state[*newTask]) == ready)
    _(ensures \result == pdPASS ==> FreeRTOS->priority[*newTask] == 
        (\natural)(uxPriority < configMAX_PRIORITIES ? uxPriority : configMAX_PRIORITIES - ( unsigned portBASE_TYPE ) 1U))
    _(ensures \result == pdPASS ==> pxCurrentTCB->\closed)
    _(ensures \result == pdPASS ==> \fresh(*newTask))
    _(ensures \forall TASK t; (FreeRTOS->tasks[t] && \old(FreeRTOS->state[t]) != FreeRTOS->state[t]) ==> transition[\old(FreeRTOS->state[t])][FreeRTOS->state[t]])
{
	_(assert \wrapped(FreeRTOS))
	_(assert \inv(FreeRTOS))
	_(assert xSchedulerRunning == pdTRUE)
	_(assert FreeRTOS->tasks[pxCurrentTCB])
	_(assert pxCurrentTCB \in FreeRTOS->\owns)
	
	//_(assert \forall TASK t; FreeRTOS->tasks[t] ==> (t \in FreeRTOS->\owns && t->\closed))
	//_(assert \forall TASK t; FreeRTOS->tasks[t] ==> t->\closed)
	_(assert \forall TASK t; FreeRTOS->tasks[t] ==> \inv(t))
	//_(assert \forall TASK t; FreeRTOS->tasks[t] ==> FreeRTOS->priority[t] == t->uxPriority)
	_(assert \forall TASK t; FreeRTOS->tasks[t] ==> FreeRTOS->priority[t] < configMAX_PRIORITIES)

	_(assert \forall TASK t; FreeRTOS->tasks[t] ==> FreeRTOS->state[t] <= 4)
	_(assert pxCurrentTCB->\closed)

	signed portBASE_TYPE xReturn;
	tskTCB * pxNewTCB;

	pxNewTCB = (tskTCB *) malloc(sizeof(tskTCB));

		_(assert pxNewTCB != pxCurrentTCB)
		//_(assert \wrapped(pxCurrentTCB))

		if ( pxNewTCB != NULL )
		{
			_(assert pxNewTCB)
			_(assert \fresh(pxNewTCB))
            
		    /* Setup the newly allocated TCB with the initial state of the task. */
			//prvInitialiseTCBVariables( pxNewTCB, pcName, uxPriority, xRegions, usStackDepth );
			
            pxNewTCB->uxPriority = (uxPriority < configMAX_PRIORITIES ? uxPriority : configMAX_PRIORITIES - ( unsigned portBASE_TYPE ) 1U);
            pxNewTCB->xGenericListItem.pvContainer = &pxReadyTasksLists[pxNewTCB->uxPriority];
            
            _(assert \writable(&(pxNewTCB->xGenericListItem)))
		    _(assert \writable(&(pxNewTCB->xEventListItem)))
		    _(wrap &(pxNewTCB->xGenericListItem))
		    _(wrap &(pxNewTCB->xEventListItem))

            _(ghost pxNewTCB->\owns = (\objset) {&(pxNewTCB->xGenericListItem)})
            _(ghost pxNewTCB->\owns += &(pxNewTCB->xEventListItem))

            _(assert !(FreeRTOS \in pxNewTCB->\owns))
            _(wrap pxNewTCB)

            if ( ( void * ) pxCreatedTask != NULL )
            {
                *pxCreatedTask = ( xTaskHandle ) pxNewTCB;
            }

            //_(assert \false)
            taskENTER_CRITICAL();
            {
                //...
                xReturn = pdPASS;
            }
            taskEXIT_CRITICAL();
		}
		else
		{
            _(assert \inv(FreeRTOS))
			xReturn = errCOULD_NOT_ALLOCATE_REQUIRED_MEMORY;
		}

        if( xReturn == pdPASS )
        {
            _(unwrapping FreeRTOS){
                _(assert \inv(FreeRTOS))

                _(ghost {
                    FreeRTOS->priority[(TASK) pxNewTCB] = pxNewTCB->uxPriority;
                    FreeRTOS->state[(TASK) pxNewTCB] = ready;
                    FreeRTOS->tasks[(TASK) pxNewTCB] = \true;
                    FreeRTOS->\owns += pxNewTCB;
                    *newTask = pxNewTCB;
                })
                    
                _(assert FreeRTOS->state[(TASK) pxNewTCB] == ready)
                _(assert FreeRTOS->state[(TASK) pxCurrentTCB] == running)
                _(assert FreeRTOS->priority[(TASK) pxNewTCB] == pxNewTCB->uxPriority)
                _(assert \forall TASK t; (FreeRTOS->tasks[t] && ((tskTCB *)t != pxNewTCB) && xSchedulerRunning != pdFALSE) ==>
                    (
                        (((xList *)((tskTCB *) t)->xGenericListItem.pvContainer) == &pxReadyTasksLists[((tskTCB *) t)->uxPriority] &&
                        ((tskTCB *) t) != pxCurrentTCB) <==> FreeRTOS->state[t] == ready
                    )
                )

                _(assert \forall TASK t; (FreeRTOS->tasks[t] && ((tskTCB *)t != pxNewTCB) && xSchedulerRunning != pdFALSE) ==>
                    (
                        (((xList *)((tskTCB *) t)->xGenericListItem.pvContainer) == &xDelayedTaskList1 ||
                         ((xList *)((tskTCB *) t)->xGenericListItem.pvContainer) == &xDelayedTaskList2)
                            <==> FreeRTOS->state[t] == blocked
                    )
                )

                _(assert \forall TASK t; (FreeRTOS->tasks[t] && ((tskTCB *)t != pxNewTCB) && xSchedulerRunning != pdFALSE) ==>
                    (
                        ((xList *)((tskTCB *) t)->xGenericListItem.pvContainer) == &xSuspendedTaskList
                            <==> FreeRTOS->state[t] == suspended
                    )
                )

                _(assert \forall TASK t; (t->\closed && ((tskTCB *)t != pxNewTCB) && xSchedulerRunning != pdFALSE) ==>
                    (
                        (((xList *)((tskTCB *) t)->xGenericListItem.pvContainer) == &xTasksWaitingTermination ||
                          t == NULL) 
                            <==> FreeRTOS->state[t] == nonexistent
                    )
                )


                if( _(atomic_read \embedding(&pxCurrentTCB))
                    pxCurrentTCB->uxPriority < uxPriority )
                {
                    _(ghost {
                        FreeRTOS->state[(TASK) pxCurrentTCB] = ready;
                        FreeRTOS->state[(TASK) pxNewTCB] = running;
                    })
                        
                    _(assert FreeRTOS->state[(TASK) \old(pxCurrentTCB)] == ready)
                    
                    //portYIELD_WITHIN_API();
                    _(atomic \embedding(&pxCurrentTCB)){
                        pxCurrentTCB = pxNewTCB;
                        _(bump_volatile_version \embedding(&pxCurrentTCB))
                    }
                }
                
                _(assert \old(pxCurrentTCB)->uxPriority >= uxPriority ==> (FreeRTOS->state[(TASK) pxNewTCB] == ready && FreeRTOS->state[(TASK) pxCurrentTCB] == running))
                _(assert \old(pxCurrentTCB)->uxPriority < uxPriority ==>
                    (FreeRTOS->state[(TASK) pxNewTCB] == running &&
                        pxNewTCB == pxCurrentTCB &&
                        FreeRTOS->state[(TASK) \old(pxCurrentTCB)] == ready
                    )
                )
                _(assert FreeRTOS->priority[(TASK) pxNewTCB] == pxNewTCB->uxPriority)
                _(assert FreeRTOS->priority[(TASK) \old(pxCurrentTCB)] == \old(pxCurrentTCB)->uxPriority)
                _(assert FreeRTOS->tasks[(TASK) \old(pxCurrentTCB)])

                _(assume \forall TASK t; (FreeRTOS->tasks[t] && ((tskTCB *)t != pxNewTCB) && xSchedulerRunning != pdFALSE) ==>
                    (
                        (((xList *)((tskTCB *) t)->xGenericListItem.pvContainer) == &pxReadyTasksLists[((tskTCB *) t)->uxPriority] &&
                        ((tskTCB *) t) != pxCurrentTCB)
                            <==> FreeRTOS->state[t] == ready
                    )
                )

                _(assume \forall TASK t; (FreeRTOS->tasks[t] && ((tskTCB *)t != pxNewTCB) && xSchedulerRunning != pdFALSE) ==>
                    (
                        (((xList *)((tskTCB *) t)->xGenericListItem.pvContainer) == &xDelayedTaskList1 ||
                         ((xList *)((tskTCB *) t)->xGenericListItem.pvContainer) == &xDelayedTaskList2)
                            <==> FreeRTOS->state[t] == blocked
                    )
                )

                _(assume \forall TASK t; (FreeRTOS->tasks[t] && ((tskTCB *)t != pxNewTCB) && xSchedulerRunning != pdFALSE) ==>
                    (
                        ((xList *)((tskTCB *) t)->xGenericListItem.pvContainer) == &xSuspendedTaskList
                            <==> FreeRTOS->state[t] == suspended
                    )
                )

                _(assume \forall TASK t; (t->\closed && ((tskTCB *)t != pxNewTCB) && xSchedulerRunning != pdFALSE) ==>
                    (
                        (((xList *)((tskTCB *) t)->xGenericListItem.pvContainer) == &xTasksWaitingTermination ||
                          t == NULL) 
                            <==> FreeRTOS->state[t] == nonexistent
                    )
                )

                _(assert \forall TASK t; FreeRTOS->tasks[t] ==> t->\closed)


                //_(assume \inv(FreeRTOS))
            }//wrapping FreeRTOS

        }
    _(assume Trans())
    return xReturn;
}

void vTaskDelete( xTaskHandle pxTaskToDelete _(ghost FRTOS FreeRTOS) _(ghost TASK topReady))
    _(updates FreeRTOS)
    _(requires \mutable(&xSchedulerRunning))
    _(requires xSchedulerRunning == pdTRUE)
    _(requires excList())

    _(requires FreeRTOS->tasks[(TASK) pxTaskToDelete])
    _(requires (tskTCB *)pxTaskToDelete != (tskTCB *)xIdleTaskHandle)

    _(requires FreeRTOS->tasks[topReady])
    _(requires FreeRTOS->state[topReady] == ready)
    _(requires \forall TASK rts;
        (FreeRTOS->tasks[rts] && FreeRTOS->state[rts] == ready)
            ==> FreeRTOS->priority[topReady] >= FreeRTOS->priority[rts])
    _(requires topReady != (TASK) pxTaskToDelete)
    _(requires topReady != (TASK) pxCurrentTCB)
    
    _(ensures ((TASK) pxTaskToDelete)->\closed)
    _(ensures pxTaskToDelete != NULL ==> ! FreeRTOS->tasks[(TASK) pxTaskToDelete])
    _(ensures pxTaskToDelete == NULL ==> ! FreeRTOS->tasks[(TASK) \old(pxCurrentTCB)])
    _(ensures pxTaskToDelete == NULL ==> (TASK) pxCurrentTCB == topReady)
    _(ensures \forall TASK t; (FreeRTOS->tasks[t] && \old(FreeRTOS->state[t]) != FreeRTOS->state[t]) ==> transition[\old(FreeRTOS->state[t])][FreeRTOS->state[t]])
{
    _(assert \wrapped(FreeRTOS))
    _(assert \inv(FreeRTOS))
    _(assert xSchedulerRunning == pdTRUE)
    //_(assert FreeRTOS->tasks[(TASK) pxTaskToDelete])
    //_(assert pxCurrentTCB \in FreeRTOS->\owns)
    _(assert \forall TASK t; FreeRTOS->tasks[t] ==> \inv(t))
    _(assert \forall TASK t; FreeRTOS->tasks[t] ==> FreeRTOS->priority[t] < configMAX_PRIORITIES)
    _(assert \forall TASK t; FreeRTOS->tasks[t] ==> FreeRTOS->state[t] <= 4)
    _(assert pxCurrentTCB->\closed)
    _(assert ((TASK)pxTaskToDelete)->\closed)

    tskTCB *pxTCB;
    
    _(unwrapping FreeRTOS){
        taskENTER_CRITICAL();
        {
            _(assert \inv(FreeRTOS))
            ///* Ensure a yield is performed if the current task is being
            //deleted. */
            //

            if ( pxTaskToDelete == _(atomic_read \embedding(&pxCurrentTCB))
                                   pxCurrentTCB )
            {
                pxTaskToDelete = NULL;
            }

            //
		    ///* If null is passed in here then we are deleting ourselves. */
            // _(atomic \embedding(&pxCurrentTCB)){
            pxTCB = _(atomic_read \embedding(&pxCurrentTCB))
                    prvGetTCBFromHandle( pxTaskToDelete );
                // pxTCB = pxTaskToDelete != NULL ? (tskTCB *) pxTaskToDelete
                //                                : pxCurrentTCB;
            // }
            _(assert (TASK) pxTaskToDelete == (TASK) pxCurrentTCB ==>
                    pxTCB == pxCurrentTCB)
            _(assert \wrapped(pxTCB))

            _(unwrapping pxTCB){
			    /* Remove task from the ready list and place in the	termination list.
			    This will stop the task from be scheduled.  The idle task will check
			    the termination list and free up any memory allocated by the
			    scheduler for the TCB and stack. */

			    _(assert \wrapped(&(pxTCB->xGenericListItem)))
                if( uxListRemove( ( xListItem * ) &( pxTCB->xGenericListItem ) ) == 0 )
			    {
				    //taskRESET_READY_PRIORITY( pxTCB->uxPriority );
			    }

                //_(assert \wrapped(&(pxTCB->xGenericListItem)))
                //_(unwrapping &(pxTCB->xGenericListItem)) {
                //    pxTCB->xGenericListItem.pvContainer = NULL;
                //}

                _(assert pxTCB->xGenericListItem.pvContainer == NULL)
                 
			    /* Is the task waiting on an event also? */
			    if( pxTCB->xEventListItem.pvContainer != NULL )
			    {
				    uxListRemove( &( pxTCB->xEventListItem ) );
			    }

                _(assert pxTCB->xEventListItem.pvContainer == NULL)

                vListInsertEnd( ( xList * ) &xTasksWaitingTermination, &( pxTCB->xGenericListItem ) );
                _(assert (xList *)(pxTCB->xGenericListItem.pvContainer) == (xList *) &xTasksWaitingTermination)
            }

            _(ghost {
                FreeRTOS->state[(TASK) pxTCB] = nonexistent;
                FreeRTOS->tasks[(TASK) pxTCB] = \false;
            })

        }
        taskEXIT_CRITICAL();

        _(assert \forall TASK t; (FreeRTOS->tasks[t] && ((tskTCB *)t != pxTCB) && xSchedulerRunning != pdFALSE) ==>
            (
                (((xList *)((tskTCB *) t)->xGenericListItem.pvContainer) == &pxReadyTasksLists[((tskTCB *) t)->uxPriority] &&
                ((tskTCB *) t) != pxCurrentTCB)
                    <==> FreeRTOS->state[t] == ready
            )
        )

        _(assert \forall TASK t; (FreeRTOS->tasks[t] && ((tskTCB *)t != pxTCB) && xSchedulerRunning != pdFALSE) ==>
            (
                (((xList *)((tskTCB *) t)->xGenericListItem.pvContainer) == &xDelayedTaskList1 ||
                    ((xList *)((tskTCB *) t)->xGenericListItem.pvContainer) == &xDelayedTaskList2)
                    <==> FreeRTOS->state[t] == blocked
            )
        )

        _(assert \forall TASK t; (FreeRTOS->tasks[t] && ((tskTCB *)t != pxTCB) && xSchedulerRunning != pdFALSE) ==>
            (
                ((xList *)((tskTCB *) t)->xGenericListItem.pvContainer) == &xSuspendedTaskList
                    <==> FreeRTOS->state[t] == suspended
            )
        )

        //_(assert \forall TASK t; (t->\closed && ((tskTCB *)t != pxTCB) && xSchedulerRunning != pdFALSE) ==>
        //    (
        //        (((xList *)((tskTCB *) t)->xGenericListItem.pvContainer) == &xTasksWaitingTermination ||
        //            t == NULL) 
        //            <==> FreeRTOS->state[t] == nonexistent
        //    )
        //)

        /* Force a reschedule if we have just deleted the current task. */

		if( xSchedulerRunning != pdFALSE )
		{
			if( ( void * ) pxTaskToDelete == NULL )
			{
				//portYIELD_WITHIN_API();
                _(atomic \embedding(&pxCurrentTCB)){
                    _(ghost pxCurrentTCB = topReady)
                    _(bump_volatile_version \embedding(&pxCurrentTCB))
                }
                _(ghost FreeRTOS->state[topReady] = running)
                
                _(assert FreeRTOS->state[(TASK) pxTCB] == nonexistent)
                _(assert (xList *)(pxTCB->xGenericListItem.pvContainer) == &xTasksWaitingTermination)
                _(assert !FreeRTOS->tasks[(TASK) pxTCB])

                _(assert FreeRTOS->state[(TASK) pxCurrentTCB] == running)
                _(assert \old(pxCurrentTCB) == pxTCB)
                _(assert FreeRTOS->state[(TASK) \old(pxCurrentTCB)] == nonexistent)
			}
		}

        _(assert pxTaskToDelete != NULL ==> FreeRTOS->state[topReady] == ready)
            
        _(assume \forall TASK t; (FreeRTOS->tasks[t] && ((tskTCB *)t != pxTCB) && xSchedulerRunning != pdFALSE) ==>
            (
                (((xList *)((tskTCB *) t)->xGenericListItem.pvContainer) == &pxReadyTasksLists[((tskTCB *) t)->uxPriority] &&
                ((tskTCB *) t) != pxCurrentTCB)
                    <==> FreeRTOS->state[t] == ready
            )
        )

        _(assume \forall TASK t; (FreeRTOS->tasks[t] && ((tskTCB *)t != pxTCB) && xSchedulerRunning != pdFALSE) ==>
            (
                (((xList *)((tskTCB *) t)->xGenericListItem.pvContainer) == &xDelayedTaskList1 ||
                    ((xList *)((tskTCB *) t)->xGenericListItem.pvContainer) == &xDelayedTaskList2)
                    <==> FreeRTOS->state[t] == blocked
            )
        )

        _(assume \forall TASK t; (FreeRTOS->tasks[t] && ((tskTCB *)t != pxTCB) && xSchedulerRunning != pdFALSE) ==>
            (
                ((xList *)((tskTCB *) t)->xGenericListItem.pvContainer) == &xSuspendedTaskList
                    <==> FreeRTOS->state[t] == suspended
            )
        )

        _(assume \forall TASK t; (t->\closed && ((tskTCB *)t != pxTCB) && xSchedulerRunning != pdFALSE) ==>
            (
                (((xList *)((tskTCB *) t)->xGenericListItem.pvContainer) == &xTasksWaitingTermination ||
                    t == NULL) 
                    <==> FreeRTOS->state[t] == nonexistent
            )
        )

        _(assert \forall TASK t; FreeRTOS->tasks[t] ==> t->\closed)

    }

    _(assume Trans())
    //_(assert \false)
}

#if ( INCLUDE_uxTaskPriorityGet == 1 )

	unsigned portBASE_TYPE uxTaskPriorityGet( xTaskHandle pxTask _(ghost FRTOS FreeRTOS))
        _(maintains \wrapped(FreeRTOS))
        _(requires FreeRTOS->tasks[(TASK) pxTask])
        _(requires xSchedulerRunning == pdTRUE)
        _(requires excList())

        _(writes FreeRTOS)
        
        _(ensures \result == FreeRTOS->priority[(TASK) pxTask])
	{
	tskTCB *pxTCB;
	unsigned portBASE_TYPE uxReturn;

		taskENTER_CRITICAL();
		{
			/* If null is passed in here then we are changing the
			priority of the calling function. */
			//pxTCB = prvGetTCBFromHandle( pxTask );
            
            _(unwrapping FreeRTOS){
                _(assert \inv(FreeRTOS))
                pxTCB = pxTask != NULL ? (tskTCB *) pxTask
                                       : pxCurrentTCB;

                _(assert \wrapped(pxTCB))
                uxReturn = pxTCB->uxPriority;
            }
		}
		taskEXIT_CRITICAL();

		return uxReturn;
	}

#endif

#if ( INCLUDE_vTaskPrioritySet == 1 )

    void vTaskPrioritySet( xTaskHandle pxTask, unsigned portBASE_TYPE uxNewPriority _(ghost FRTOS FreeRTOS) _(ghost TASK topReady) )
        _(updates FreeRTOS)
        _(requires \mutable(&xSchedulerRunning))
        _(requires xSchedulerRunning == pdTRUE)
        _(requires excList())

        _(requires FreeRTOS->tasks[topReady])
        //_(requires FreeRTOS->state[topReady] == ready)
        //_(requires \forall TASK rts;
        //    (FreeRTOS->tasks[rts] && FreeRTOS->state[rts] == ready)
        //        ==> FreeRTOS->priority[topReady] >= FreeRTOS->priority[rts])
        //_(requires topReady != (TASK) pxTask)
        //_(requires topReady != (TASK) pxCurrentTCB)

        _(requires FreeRTOS->tasks[(TASK) pxTask])
        _(requires (tskTCB *) pxTask == (tskTCB *) xIdleTaskHandle ==> uxNewPriority == 0)


        _(ensures ((TASK) pxTask)->\closed)
        _(ensures FreeRTOS->tasks[(TASK) pxTask])
        _(ensures FreeRTOS->priority[(TASK) pxTask] == 
            (\natural)(uxNewPriority < configMAX_PRIORITIES ? uxNewPriority : configMAX_PRIORITIES - ( unsigned portBASE_TYPE ) 1U))
        _(ensures (FreeRTOS->state[(TASK) pxTask] == ready && FreeRTOS->priority[(TASK) pxTask] > \old(pxCurrentTCB)->uxPriority) ==>
            (FreeRTOS->state[(TASK) \old(pxCurrentTCB)] == ready && FreeRTOS->state[(TASK) pxTask] == running)
        )
        _(ensures ((pxTask == NULL || (tskTCB *) pxTask == \old(pxCurrentTCB)) && !(
                \forall TASK t; FreeRTOS->state[t] == ready ==> FreeRTOS->priority[(TASK) pxTask] >= FreeRTOS->priority[t]
            )) ==> (FreeRTOS->state[(TASK) \old(pxCurrentTCB)] == ready &&
                    FreeRTOS->state[(TASK) pxCurrentTCB] == running &&
                    \old(FreeRTOS->state[(TASK) pxCurrentTCB]) == ready)
        )
        _(ensures \forall TASK t; (FreeRTOS->tasks[t] && \old(FreeRTOS->state[t]) != FreeRTOS->state[t]) ==> transition[\old(FreeRTOS->state[t])][FreeRTOS->state[t]])
    {
        _(assert \inv(FreeRTOS))
        _(assert xSchedulerRunning == pdTRUE)
        _(assert FreeRTOS->tasks[pxCurrentTCB])
        _(assert pxTask != NULL ==> FreeRTOS->tasks[(TASK) pxTask])
        _(assert \forall TASK t; FreeRTOS->tasks[t] ==> \inv(t))
        _(assert \forall TASK t; FreeRTOS->tasks[t] ==> FreeRTOS->priority[t] < configMAX_PRIORITIES)
        _(assert \forall TASK t; FreeRTOS->tasks[t] ==> FreeRTOS->state[t] <= 4)
        _(assert pxCurrentTCB->\closed)
        _(assert pxCurrentTCB \in FreeRTOS->\owns)
        _(assert pxTask != NULL ==> ((TASK) pxTask)->\closed)
        _(assert pxTask != NULL ==> ((TASK) pxTask) \in FreeRTOS->\owns)

        tskTCB *pxTCB;
        unsigned portBASE_TYPE uxCurrentPriority, uxPriorityUsedOnEntry;
        portBASE_TYPE xYieldRequired = pdFALSE;
        
		/* Ensure the new priority is valid. */
		if( uxNewPriority >= configMAX_PRIORITIES )
		{
			uxNewPriority = configMAX_PRIORITIES - ( unsigned portBASE_TYPE ) 1U;
		}
        _(assert uxNewPriority < configMAX_PRIORITIES)
 
        taskENTER_CRITICAL();
        {
            _(unwrapping FreeRTOS){
                _(assert \inv(FreeRTOS))
                _(assert \forall TASK t; (t->\closed && xSchedulerRunning != pdFALSE) ==> 
                    ((((xList *)((tskTCB *) t)->xGenericListItem.pvContainer) == &xTasksWaitingTermination ||
                        t == NULL) <==> FreeRTOS->state[t] == nonexistent))

                if ( pxTask == _(atomic_read \embedding(&pxCurrentTCB))
                               pxCurrentTCB)
                {
                    pxTask = NULL;
                }

                // _(atomic \embedding(&pxCurrentTCB)){
                    // pxTCB = pxTask != NULL ? (tskTCB *) pxTask
                    //                        : pxCurrentTCB;
                pxTCB = _(atomic_read \embedding(&pxCurrentTCB))
                        prvGetTCBFromHandle ( pxTask );
                // }
                
                _(assert (TASK) pxTask == (TASK) pxCurrentTCB ==>
                    pxTCB == pxCurrentTCB)

               

                //#if ( configUSE_MUTEXES == 1 )
			    //{
				   // uxCurrentPriority = pxTCB->uxBasePriority;
			    //}
			    //#else
			    //{
				    uxCurrentPriority = pxTCB->uxPriority;
			    //}
			    //#endif

                if ( uxCurrentPriority != uxNewPriority )
                {
                    /* The priority change may have readied a task of higher
				    priority than the calling task. */
                    
                    if ( uxNewPriority > uxCurrentPriority )
                    {
                        if ( pxTask != NULL )
                        {
                            /* The priority of another task is being raised.  If we
						    were raising the priority of the currently running task
						    there would be no need to switch as it must have already
						    been the highest priority task. */
                            xYieldRequired = pdTRUE;
                        }
                    }
                    else if ( pxTask == NULL )
                    {
                        /* Setting our own priority down means there may now be another
					    task of higher priority that is ready to execute. */
                        xYieldRequired = pdTRUE;
                    }
                }

                uxPriorityUsedOnEntry = pxTCB->uxPriority;

                //#if ( configUSE_MUTEXES == 1 )
                //{{

                //	/* Only change the priority being used if the task is not
                //	currently using an inherited priority. */
                //	if( pxTCB->uxBasePriority == pxTCB->uxPriority )
                //	{
                //		pxTCB->uxPriority = uxNewPriority;
                //	}

                //	/* The base priority gets set whatever. */
                //	pxTCB->uxBasePriority = uxNewPriority;
                //}
                //#else
                //{
                
                _(assert \wrapped(pxCurrentTCB))
                _(assert pxTask != NULL ==> FreeRTOS->tasks[(TASK) pxTask])
                _(assert pxTask != NULL ==> \wrapped((TASK) pxTask))
                _(assert \wrapped(pxTCB))
                _(unwrapping pxTCB){
                    
                    pxTCB->uxPriority = uxNewPriority;
                   
                    _(ghost FreeRTOS->priority[(TASK) pxTCB] = uxNewPriority)
                    _(assert FreeRTOS->priority[(TASK) pxTCB] == pxTCB->uxPriority)
                //}
                //#endif
                    /* If the task is in the blocked or suspended list we need do
				    nothing more than change it's priority variable. However, if
				    the task is in a ready list it needs to be removed and placed
				    in the queue appropriate to its new priority. */
				    //if( listIS_CONTAINED_WITHIN( &( pxReadyTasksLists[ uxCurrentPriority ] ), &( pxTCB->xGenericListItem ) ) )
                    if ( (xList *) pxTCB->xGenericListItem.pvContainer == &( pxReadyTasksLists[ uxCurrentPriority ] ))
                    {
                        //_(assert (xList *) pxTCB->xGenericListItem.pvContainer == &( pxReadyTasksLists[ uxCurrentPriority ] ))
                        //_(assert (xList *) pxTCB->xGenericListItem.pvContainer == &( pxReadyTasksLists[ uxCurrentPriority ] ) <==>
                        //    (FreeRTOS->state[(TASK) pxTCB] == running || FreeRTOS->state[(TASK) pxTCB] == ready)
                        //) 
                        _(assert FreeRTOS->state[(TASK) pxTCB] == running || FreeRTOS->state[(TASK) pxTCB] == ready)
                        /* The task is currently in its ready list - remove before adding
					    it to it's new ready list.  As we are in a critical section we
					    can do this even if the scheduler is suspended. */
					    _(assert \wrapped(&(pxTCB->xGenericListItem)))
                        if ( uxListRemove( ( xListItem * ) &( pxTCB->xGenericListItem ) ) == 0 )
                        {
                            //taskRESET_READY_PRIORITY( uxPriorityUsedOnEntry );
                        }
                        //prvAddTaskToReadyQueue( pxTCB );
                        _(assert (&(pxTCB->xGenericListItem))->\closed)
                        _(unwrapping &(pxTCB->xGenericListItem)){
                            pxTCB->xGenericListItem.pvContainer = (xList *) &( pxReadyTasksLists[pxTCB->uxPriority] );
                        }

                        _(assert FreeRTOS->tasks[(TASK) pxTCB])

                        _(assert (xList *) pxTCB->xGenericListItem.pvContainer == &( pxReadyTasksLists[ pxTCB->uxPriority ] ))
                        _(assert FreeRTOS->state[(TASK) pxTCB] == running || FreeRTOS->state[(TASK) pxTCB] == ready)
                    }
                    
                    _(assert (FreeRTOS->state[(TASK) pxTCB] == running || FreeRTOS->state[(TASK) pxTCB] == ready) ==>
                        (xList *) pxTCB->xGenericListItem.pvContainer == &( pxReadyTasksLists[ pxTCB->uxPriority ] ))
                    
                    if( xYieldRequired == pdTRUE )
                    {
                        _(assert FreeRTOS->tasks[topReady])

                        _(assume FreeRTOS->state[topReady] == ready ||
                            topReady == (TASK) pxCurrentTCB)
                        _(assume \forall TASK t; (FreeRTOS->state[t] == ready || FreeRTOS->state[t] == running)  ==>
                            FreeRTOS->priority[topReady] >= FreeRTOS->priority[t])
                        _(assume FreeRTOS->priority[topReady] == FreeRTOS->priority[(TASK) pxCurrentTCB]
                            ==> topReady == (TASK) pxCurrentTCB)

                        _(ghost {
                            FreeRTOS->state[(TASK) pxCurrentTCB] = ready;
                            FreeRTOS->state[topReady] = running;
                        })

                        //portYIELD_WITHIN_API();
                        _(atomic \embedding(&pxCurrentTCB)){
                            _(ghost pxCurrentTCB = topReady)
                            _(bump_volatile_version \embedding(&pxCurrentTCB))
                        }
                        _(assert topReady != \old((TASK) pxCurrentTCB) ==> FreeRTOS->state[(TASK) \old(pxCurrentTCB)] == ready)
                    }

                }//wrapping pxTCB
                //_(assert \false)

                _(assume \forall TASK t; (FreeRTOS->tasks[t] && ((tskTCB *)t != pxTCB) && xSchedulerRunning != pdFALSE) ==>
                    (
                        (((xList *)((tskTCB *) t)->xGenericListItem.pvContainer) == &pxReadyTasksLists[((tskTCB *) t)->uxPriority] &&
                        ((tskTCB *) t) != pxCurrentTCB)
                            <==> FreeRTOS->state[t] == ready
                    )
                )

                _(assume \forall TASK t; (FreeRTOS->tasks[t] && ((tskTCB *)t != pxTCB) && xSchedulerRunning != pdFALSE) ==>
                    (
                        (((xList *)((tskTCB *) t)->xGenericListItem.pvContainer) == &xDelayedTaskList1 ||
                            ((xList *)((tskTCB *) t)->xGenericListItem.pvContainer) == &xDelayedTaskList2)
                            <==> FreeRTOS->state[t] == blocked
                    )
                )

                _(assume \forall TASK t; (FreeRTOS->tasks[t] && ((tskTCB *)t != pxTCB) && xSchedulerRunning != pdFALSE) ==>
                    (
                        ((xList *)((tskTCB *) t)->xGenericListItem.pvContainer) == &xSuspendedTaskList
                            <==> FreeRTOS->state[t] == suspended
                    )
                )

                _(assume \forall TASK t; (t->\closed && ((tskTCB *)t != pxTCB) && xSchedulerRunning != pdFALSE) ==>
                    (
                        (((xList *)((tskTCB *) t)->xGenericListItem.pvContainer) == &xTasksWaitingTermination ||
                            t == NULL) 
                            <==> FreeRTOS->state[t] == nonexistent
                    )
                )

            }//wrapping FreeRTOS

            _(assert \inv(FreeRTOS))
        }
        taskEXIT_CRITICAL();
        _(assume Trans())
    }

#endif